(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 4))
(let ((e4 4))
(let ((e5 13))
(let ((e6 (- v1)))
(let ((e7 (- e6 v1)))
(let ((e8 (+ e7 v2)))
(let ((e9 (/ e4 (- e5))))
(let ((e10 (* e8 (- e5))))
(let ((e11 (* e8 v2)))
(let ((e12 (+ e8 v1)))
(let ((e13 (/ e4 (- e5))))
(let ((e14 (- e11 v1)))
(let ((e15 (- e8)))
(let ((e16 (/ e5 e4)))
(let ((e17 (* e14 e8)))
(let ((e18 (/ e5 e5)))
(let ((e19 (- e14)))
(let ((e20 (- v2 e8)))
(let ((e21 (/ e5 (- e4))))
(let ((e22 (/ e5 (- e5))))
(let ((e23 (* e20 e12)))
(let ((e24 (* v0 e19)))
(let ((e25 (- e23 e22)))
(let ((e26 (* e5 e19)))
(let ((e27 (- e8)))
(let ((e28 (+ e7 e21)))
(let ((e29 (- e25)))
(let ((e30 (/ e3 (- e5))))
(let ((e31 (>= e13 e20)))
(let ((e32 (> e16 e9)))
(let ((e33 (= e20 e13)))
(let ((e34 (< e16 e7)))
(let ((e35 (> e23 e10)))
(let ((e36 (>= e23 e27)))
(let ((e37 (< v2 e19)))
(let ((e38 (< e7 e14)))
(let ((e39 (<= e12 e28)))
(let ((e40 (distinct v2 e21)))
(let ((e41 (< e7 e16)))
(let ((e42 (> e19 v0)))
(let ((e43 (distinct e29 e7)))
(let ((e44 (< e28 e24)))
(let ((e45 (<= e8 e14)))
(let ((e46 (> e26 e27)))
(let ((e47 (< e29 e22)))
(let ((e48 (= e12 e16)))
(let ((e49 (= e16 e10)))
(let ((e50 (= e23 e7)))
(let ((e51 (< e22 e24)))
(let ((e52 (<= v2 e24)))
(let ((e53 (distinct e23 e18)))
(let ((e54 (distinct e24 e29)))
(let ((e55 (>= e6 e9)))
(let ((e56 (> e25 e7)))
(let ((e57 (>= e20 e9)))
(let ((e58 (<= e25 e11)))
(let ((e59 (distinct e18 e20)))
(let ((e60 (<= e25 e19)))
(let ((e61 (distinct e15 e21)))
(let ((e62 (<= e22 v1)))
(let ((e63 (distinct e7 e18)))
(let ((e64 (>= e10 e18)))
(let ((e65 (>= e25 e30)))
(let ((e66 (distinct e29 e18)))
(let ((e67 (>= e14 e30)))
(let ((e68 (distinct e30 e20)))
(let ((e69 (> e24 e20)))
(let ((e70 (> e13 e28)))
(let ((e71 (> e11 e30)))
(let ((e72 (>= e6 e20)))
(let ((e73 (distinct e10 e22)))
(let ((e74 (> e23 e30)))
(let ((e75 (= e7 e20)))
(let ((e76 (<= e7 e23)))
(let ((e77 (< e15 e10)))
(let ((e78 (> e28 e30)))
(let ((e79 (> v2 e21)))
(let ((e80 (distinct e16 e26)))
(let ((e81 (< e10 e10)))
(let ((e82 (<= e15 e30)))
(let ((e83 (<= e6 e7)))
(let ((e84 (> e28 e22)))
(let ((e85 (< e9 e6)))
(let ((e86 (>= e13 e24)))
(let ((e87 (>= v2 e13)))
(let ((e88 (> e15 e7)))
(let ((e89 (>= e6 v1)))
(let ((e90 (> e22 e14)))
(let ((e91 (>= e23 e12)))
(let ((e92 (>= e8 e22)))
(let ((e93 (<= e22 e8)))
(let ((e94 (<= e30 e24)))
(let ((e95 (>= e9 e14)))
(let ((e96 (<= e30 e21)))
(let ((e97 (>= v1 v1)))
(let ((e98 (< e26 e28)))
(let ((e99 (>= e23 e30)))
(let ((e100 (= e12 e22)))
(let ((e101 (<= e27 e24)))
(let ((e102 (distinct v0 e13)))
(let ((e103 (>= v2 e24)))
(let ((e104 (>= e16 e27)))
(let ((e105 (>= e9 e21)))
(let ((e106 (< e9 e23)))
(let ((e107 (< e29 e26)))
(let ((e108 (distinct e24 e21)))
(let ((e109 (<= e25 e8)))
(let ((e110 (distinct e25 v0)))
(let ((e111 (> e28 e8)))
(let ((e112 (distinct e25 v0)))
(let ((e113 (> e21 e22)))
(let ((e114 (< e12 e27)))
(let ((e115 (> e27 e7)))
(let ((e116 (distinct e11 e22)))
(let ((e117 (> e20 e22)))
(let ((e118 (distinct e26 e13)))
(let ((e119 (distinct e30 e11)))
(let ((e120 (< e13 e12)))
(let ((e121 (= e26 e21)))
(let ((e122 (> e12 e29)))
(let ((e123 (< e6 e12)))
(let ((e124 (< e18 e23)))
(let ((e125 (< e30 e28)))
(let ((e126 (< e15 e29)))
(let ((e127 (<= v1 v0)))
(let ((e128 (= e10 e16)))
(let ((e129 (< e10 e24)))
(let ((e130 (>= e15 e22)))
(let ((e131 (> e6 e9)))
(let ((e132 (>= v1 e8)))
(let ((e133 (> e6 e7)))
(let ((e134 (= e15 e13)))
(let ((e135 (distinct v0 e14)))
(let ((e136 (>= e25 e22)))
(let ((e137 (< e22 v0)))
(let ((e138 (>= e15 e20)))
(let ((e139 (>= e12 e23)))
(let ((e140 (<= e22 e7)))
(let ((e141 (< v2 e16)))
(let ((e142 (< e16 e23)))
(let ((e143 (<= e29 v0)))
(let ((e144 (< e26 e11)))
(let ((e145 (<= e24 e24)))
(let ((e146 (= e11 e17)))
(let ((e147 (distinct e15 v1)))
(let ((e148 (= e19 e22)))
(let ((e149 (= e21 e15)))
(let ((e150 (> e13 e12)))
(let ((e151 (< e11 e9)))
(let ((e152 (<= v0 e28)))
(let ((e153 (> e18 v2)))
(let ((e154 (< e15 e10)))
(let ((e155 (= e13 e8)))
(let ((e156 (<= e11 e9)))
(let ((e157 (>= e10 e19)))
(let ((e158 (> e7 e7)))
(let ((e159 (distinct e15 e17)))
(let ((e160 (<= e20 v1)))
(let ((e161 (= v2 e13)))
(let ((e162 (>= e16 e8)))
(let ((e163 (< v0 e11)))
(let ((e164 (> e11 e19)))
(let ((e165 (= e16 e21)))
(let ((e166 (>= e15 e9)))
(let ((e167 (= e12 e29)))
(let ((e168 (<= e16 e17)))
(let ((e169 (< e15 e10)))
(let ((e170 (< e26 e15)))
(let ((e171 (>= e24 e13)))
(let ((e172 (= e13 e16)))
(let ((e173 (< e8 e29)))
(let ((e174 (= v2 e13)))
(let ((e175 (distinct e13 e29)))
(let ((e176 (>= e17 e15)))
(let ((e177 (= e30 e14)))
(let ((e178 (distinct e20 e18)))
(let ((e179 (distinct e16 e26)))
(let ((e180 (>= e11 e20)))
(let ((e181 (> e24 v1)))
(let ((e182 (> e17 e16)))
(let ((e183 (>= e30 e12)))
(let ((e184 (<= e25 e17)))
(let ((e185 (>= e28 e30)))
(let ((e186 (> v0 e19)))
(let ((e187 (< e14 e16)))
(let ((e188 (>= e12 v2)))
(let ((e189 (<= e22 e17)))
(let ((e190 (>= e24 e8)))
(let ((e191 (> e26 e6)))
(let ((e192 (<= e26 e26)))
(let ((e193 (= e22 e11)))
(let ((e194 (< v1 e18)))
(let ((e195 (= e22 e20)))
(let ((e196 (>= e12 e7)))
(let ((e197 (> e30 e30)))
(let ((e198 (distinct e22 e8)))
(let ((e199 (distinct e16 e20)))
(let ((e200 (<= v1 v1)))
(let ((e201 (distinct e6 e22)))
(let ((e202 (< v2 e22)))
(let ((e203 (<= v2 e22)))
(let ((e204 (>= e26 e18)))
(let ((e205 (= e22 e12)))
(let ((e206 (<= e24 v2)))
(let ((e207 (>= e23 e6)))
(let ((e208 (> e24 e6)))
(let ((e209 (= e13 e15)))
(let ((e210 (= e18 e24)))
(let ((e211 (distinct e11 e13)))
(let ((e212 (< e20 e28)))
(let ((e213 (<= e16 e19)))
(let ((e214 (> e22 e25)))
(let ((e215 (distinct e11 e19)))
(let ((e216 (distinct e15 v2)))
(let ((e217 (= e18 e22)))
(let ((e218 (distinct e11 e10)))
(let ((e219 (= e9 v1)))
(let ((e220 (>= e8 e15)))
(let ((e221 (< v0 e12)))
(let ((e222 (> e28 e26)))
(let ((e223 (< e29 v0)))
(let ((e224 (= e14 e29)))
(let ((e225 (<= e9 e26)))
(let ((e226 (distinct e23 e16)))
(let ((e227 (>= e6 v1)))
(let ((e228 (>= e19 e11)))
(let ((e229 (= e15 e25)))
(let ((e230 (= e24 e7)))
(let ((e231 (= e27 e8)))
(let ((e232 (=> e64 e183)))
(let ((e233 (not e103)))
(let ((e234 (xor e147 e210)))
(let ((e235 (ite e208 e50 e72)))
(let ((e236 (not e160)))
(let ((e237 (xor e39 e82)))
(let ((e238 (and e161 e188)))
(let ((e239 (ite e235 e36 e132)))
(let ((e240 (not e228)))
(let ((e241 (= e69 e230)))
(let ((e242 (not e194)))
(let ((e243 (ite e221 e206 e87)))
(let ((e244 (xor e216 e218)))
(let ((e245 (not e111)))
(let ((e246 (= e57 e97)))
(let ((e247 (ite e37 e185 e115)))
(let ((e248 (ite e98 e130 e217)))
(let ((e249 (xor e70 e38)))
(let ((e250 (and e63 e191)))
(let ((e251 (or e124 e197)))
(let ((e252 (and e181 e58)))
(let ((e253 (or e201 e163)))
(let ((e254 (=> e116 e35)))
(let ((e255 (=> e100 e158)))
(let ((e256 (ite e246 e179 e248)))
(let ((e257 (and e204 e107)))
(let ((e258 (or e254 e177)))
(let ((e259 (and e104 e209)))
(let ((e260 (ite e172 e171 e229)))
(let ((e261 (= e247 e142)))
(let ((e262 (and e54 e237)))
(let ((e263 (and e133 e192)))
(let ((e264 (xor e33 e99)))
(let ((e265 (xor e138 e153)))
(let ((e266 (xor e114 e95)))
(let ((e267 (= e231 e128)))
(let ((e268 (xor e137 e34)))
(let ((e269 (and e249 e59)))
(let ((e270 (and e146 e220)))
(let ((e271 (not e154)))
(let ((e272 (and e113 e56)))
(let ((e273 (or e245 e239)))
(let ((e274 (=> e251 e244)))
(let ((e275 (= e257 e155)))
(let ((e276 (= e205 e52)))
(let ((e277 (not e90)))
(let ((e278 (xor e215 e131)))
(let ((e279 (= e166 e236)))
(let ((e280 (=> e91 e203)))
(let ((e281 (xor e49 e195)))
(let ((e282 (= e149 e119)))
(let ((e283 (xor e222 e44)))
(let ((e284 (= e140 e170)))
(let ((e285 (ite e269 e109 e84)))
(let ((e286 (and e62 e199)))
(let ((e287 (and e93 e40)))
(let ((e288 (= e211 e122)))
(let ((e289 (not e264)))
(let ((e290 (ite e224 e278 e53)))
(let ((e291 (not e108)))
(let ((e292 (not e168)))
(let ((e293 (=> e43 e78)))
(let ((e294 (and e260 e101)))
(let ((e295 (or e135 e110)))
(let ((e296 (= e167 e71)))
(let ((e297 (not e225)))
(let ((e298 (not e214)))
(let ((e299 (not e74)))
(let ((e300 (=> e127 e117)))
(let ((e301 (or e286 e232)))
(let ((e302 (not e80)))
(let ((e303 (= e285 e150)))
(let ((e304 (ite e261 e303 e184)))
(let ((e305 (ite e32 e207 e280)))
(let ((e306 (xor e305 e289)))
(let ((e307 (= e77 e266)))
(let ((e308 (and e156 e298)))
(let ((e309 (not e202)))
(let ((e310 (and e89 e234)))
(let ((e311 (xor e139 e308)))
(let ((e312 (=> e48 e47)))
(let ((e313 (=> e294 e227)))
(let ((e314 (and e250 e270)))
(let ((e315 (=> e276 e306)))
(let ((e316 (=> e311 e162)))
(let ((e317 (not e297)))
(let ((e318 (xor e83 e143)))
(let ((e319 (xor e186 e242)))
(let ((e320 (not e112)))
(let ((e321 (= e240 e277)))
(let ((e322 (ite e265 e85 e288)))
(let ((e323 (not e321)))
(let ((e324 (= e323 e275)))
(let ((e325 (xor e190 e102)))
(let ((e326 (and e290 e313)))
(let ((e327 (not e187)))
(let ((e328 (not e125)))
(let ((e329 (not e60)))
(let ((e330 (ite e262 e219 e134)))
(let ((e331 (or e200 e94)))
(let ((e332 (or e174 e61)))
(let ((e333 (= e65 e233)))
(let ((e334 (and e258 e213)))
(let ((e335 (=> e41 e148)))
(let ((e336 (and e212 e141)))
(let ((e337 (or e320 e312)))
(let ((e338 (or e296 e272)))
(let ((e339 (ite e331 e238 e326)))
(let ((e340 (ite e165 e336 e121)))
(let ((e341 (not e157)))
(let ((e342 (not e86)))
(let ((e343 (ite e293 e73 e152)))
(let ((e344 (not e300)))
(let ((e345 (or e256 e42)))
(let ((e346 (and e340 e76)))
(let ((e347 (xor e255 e279)))
(let ((e348 (ite e339 e271 e182)))
(let ((e349 (and e302 e316)))
(let ((e350 (not e118)))
(let ((e351 (and e198 e347)))
(let ((e352 (and e105 e81)))
(let ((e353 (= e330 e327)))
(let ((e354 (ite e301 e341 e334)))
(let ((e355 (= e169 e282)))
(let ((e356 (or e253 e284)))
(let ((e357 (and e274 e287)))
(let ((e358 (xor e96 e92)))
(let ((e359 (and e68 e342)))
(let ((e360 (ite e136 e45 e299)))
(let ((e361 (and e345 e356)))
(let ((e362 (or e88 e322)))
(let ((e363 (ite e241 e349 e304)))
(let ((e364 (=> e309 e159)))
(let ((e365 (ite e324 e355 e263)))
(let ((e366 (ite e292 e106 e307)))
(let ((e367 (not e79)))
(let ((e368 (not e252)))
(let ((e369 (ite e365 e328 e178)))
(let ((e370 (xor e46 e332)))
(let ((e371 (= e126 e368)))
(let ((e372 (or e281 e180)))
(let ((e373 (=> e310 e31)))
(let ((e374 (xor e51 e120)))
(let ((e375 (xor e348 e372)))
(let ((e376 (xor e343 e325)))
(let ((e377 (not e335)))
(let ((e378 (= e283 e337)))
(let ((e379 (= e318 e319)))
(let ((e380 (or e363 e344)))
(let ((e381 (and e351 e380)))
(let ((e382 (ite e367 e338 e123)))
(let ((e383 (and e55 e243)))
(let ((e384 (xor e226 e357)))
(let ((e385 (not e364)))
(let ((e386 (ite e223 e67 e382)))
(let ((e387 (=> e176 e383)))
(let ((e388 (or e369 e189)))
(let ((e389 (= e350 e75)))
(let ((e390 (not e267)))
(let ((e391 (= e295 e329)))
(let ((e392 (and e373 e385)))
(let ((e393 (ite e386 e374 e144)))
(let ((e394 (=> e389 e370)))
(let ((e395 (and e352 e359)))
(let ((e396 (not e379)))
(let ((e397 (= e377 e353)))
(let ((e398 (= e317 e164)))
(let ((e399 (and e390 e395)))
(let ((e400 (not e366)))
(let ((e401 (and e391 e392)))
(let ((e402 (and e291 e314)))
(let ((e403 (xor e394 e396)))
(let ((e404 (or e393 e387)))
(let ((e405 (=> e273 e381)))
(let ((e406 (=> e358 e403)))
(let ((e407 (=> e145 e388)))
(let ((e408 (xor e360 e346)))
(let ((e409 (=> e402 e333)))
(let ((e410 (xor e371 e66)))
(let ((e411 (not e404)))
(let ((e412 (=> e268 e268)))
(let ((e413 (xor e412 e397)))
(let ((e414 (not e413)))
(let ((e415 (xor e315 e193)))
(let ((e416 (not e410)))
(let ((e417 (ite e175 e415 e151)))
(let ((e418 (= e173 e196)))
(let ((e419 (not e414)))
(let ((e420 (not e129)))
(let ((e421 (xor e420 e375)))
(let ((e422 (= e401 e408)))
(let ((e423 (or e384 e409)))
(let ((e424 (= e354 e406)))
(let ((e425 (and e422 e422)))
(let ((e426 (not e416)))
(let ((e427 (= e378 e417)))
(let ((e428 (= e376 e423)))
(let ((e429 (xor e427 e418)))
(let ((e430 (and e259 e361)))
(let ((e431 (or e362 e407)))
(let ((e432 (not e426)))
(let ((e433 (or e405 e428)))
(let ((e434 (xor e400 e430)))
(let ((e435 (xor e421 e398)))
(let ((e436 (xor e424 e411)))
(let ((e437 (= e434 e429)))
(let ((e438 (xor e437 e399)))
(let ((e439 (= e433 e435)))
(let ((e440 (=> e439 e436)))
(let ((e441 (or e425 e432)))
(let ((e442 (or e431 e419)))
(let ((e443 (ite e442 e440 e440)))
(let ((e444 (not e441)))
(let ((e445 (not e444)))
(let ((e446 (and e443 e443)))
(let ((e447 (and e445 e438)))
(let ((e448 (= e446 e446)))
(let ((e449 (= e447 e448)))
e449
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
